e<e'. P(e) == e:E. (e <loc e')  P(e) 

latex

---

clarification:

alle-lt(es;e';e.P(e)) == e:es-E(es). es-locl(es; e; e')  P(e) 

latex

Definitions	x:A. B(x), E, P  Q, (e <loc e')
FDL editor aliases	alle-lt